the_w:World, i:Id, a:Action(i). ((isnull(a)))  (valtype(i;a)  Type) 

latex

Definitions	x:A. B(x), Action(i), P  Q, isnull(a), t  T, valtype(i;a), w.TA, w.M, isl(x), kind(a), t.1, t.2, outr(x), True, x. t(x), x,y. t(x;y), World, A, b, Action(dec), x(s), x(s1,s2), tt, ff, if b then t else f fi , False,
Lemmas	kindcase wf, pi1 wf, Knd wf, Id wf, IdLnk wf, not wf, assert wf, btrue wf, bfalse wf, action wf, w-action-dec wf, world wf